Example 15 in [ Lucas - IC'06]

Summary: Ex15_Luc06

• TPDB format
• OBJ format
• Negative results:
  1. Lucas'
• Positive results:
  1. CSRPO
  2. CSDP
  3. Ferreira and Ribeiro's transformation
  4. Giesl and Middeldorp's transformation
  5. Zantema's transformation

Ex15_Luc06 in TPDB format ( Ex15_Luc06.trs):

(VAR )
(STRATEGY CONTEXTSENSITIVE 
  (f)
  (a)
  (g 1)
)
(RULES 
f(f(a)) -> f(g(f(a)))
)

The CS-TRS in OBJ format (file Ex15_Luc06.obj):

obj Ex15_Luc06 is
  sort S .
  op f : S -> S [strat (0)] .
  op a : -> S .
  op g : S -> S .
  eq f(f(a)) = f(g(f(a))) .
endo

Negative results

1. The µ-termination of Ex15_Luc06 cannot be proved by using Lucas' transformation. The TRS Ex15_Luc06_L:

   	f -> f
   
   	
   

   is clearly not terminating (AProVE).
   

Positive results

1. The µ-termination of Ex15_Luc06 can be proved by using CSRPO ( MuTerm ).
2. The µ-termination of Ex15_Luc06 can be proved by using CSDPs ( MuTerm ).
3. The µ-termination of Ex15_Luc06 can be proved by using Ferreira and Ribeiro's or Zantema's transformation. The transformed TRS Ex15_Luc06:

   					
   	f(n__f(n__a)) -> f(n__g(n__f(n__a)))
   	f(X) -> n__f(X)
   	a -> n__a
   	g(X) -> n__g(X)
   	activate(n__f(X)) -> f(X)
   	activate(n__a) -> a
   	activate(n__g(X)) -> g(activate(X))
   	activate(X) -> X
   	
   	

   can be proved terminating by AProVE
4. The µ-termination of Ex15_Luc06 can be proved by using Giesl and Middeldorp's transformation. The TRS Ex15_Luc06_GM:

   					 
   	a__f(f(a)) -> a__f(g(f(a)))
   	mark(f(X)) -> a__f(X)
   	mark(a) -> a
   	mark(g(X)) -> g(mark(X))
   	a__f(X) -> f(X)
   	
   	

   can be proved terminating by AProVE